YES 12.259
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((group :: [Int] -> [[Int]]) :: [Int] -> [[Int]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule List
| ((group :: [Int] -> [[Int]]) :: [Int] -> [[Int]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((group :: [Int] -> [[Int]]) :: [Int] -> [[Int]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (ww : wx) | |
is transformed to
span | p [] | = span3 p [] |
span | p (ww : wx) | = span2 p (ww : wx) |
span2 | p (ww : wx) | =
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | xx xy | = span2 xx xy |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
| ((group :: [Int] -> [[Int]]) :: [Int] -> [[Int]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs |
where | |
| |
| |
| |
| |
are unpacked to the following functions on top level
groupByYs0 | xz yu yv (ys,vx) | = ys |
groupByZs0 | xz yu yv (vy,zs) | = zs |
groupByYs | xz yu yv | = groupByYs0 xz yu yv (groupByVv10 xz yu yv) |
groupByVv10 | xz yu yv | = span (xz yu) yv |
groupByZs | xz yu yv | = groupByZs0 xz yu yv (groupByVv10 xz yu yv) |
The bindings of the following Let/Where expression
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Ys | yw yx | = span2Ys1 yw yx (span2Vu43 yw yx) |
span2Zs | yw yx | = span2Zs1 yw yx (span2Vu43 yw yx) |
span2Zs1 | yw yx (wy,zs) | = zs |
span2Span0 | yw yx p ww wx True | = ([],ww : wx) |
span2Span1 | yw yx p ww wx True | = (ww : span2Ys yw yx,span2Zs yw yx) |
span2Span1 | yw yx p ww wx False | = span2Span0 yw yx p ww wx otherwise |
span2Vu43 | yw yx | = span yw yx |
span2Ys1 | yw yx (ys,wz) | = ys |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
| (group :: [Int] -> [[Int]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = | (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs) |
|
|
groupByVv10 | xz yu yv | = | span (xz yu) yv |
|
|
groupByYs | xz yu yv | = | groupByYs0 xz yu yv (groupByVv10 xz yu yv) |
|
|
groupByYs0 | xz yu yv (ys,vx) | = | ys |
|
|
groupByZs | xz yu yv | = | groupByZs0 xz yu yv (groupByVv10 xz yu yv) |
|
|
groupByZs0 | xz yu yv (vy,zs) | = | zs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Ys(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Ys(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(Neg(Zero), yy3111)) → new_span2Zs(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(Pos(Zero), yy3111)) → new_span2Zs(yy3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Zs0(yy376, yy378)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Zs0(yy370, yy372)
new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Ys0(yy376, yy378)
new_span2Zs0(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs1(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys0(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys1(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs1(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs1(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Ys0(yy370, yy372)
new_span2Ys1(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys1(yy370, yy371, yy372, yy3730, yy3740)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs0(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs1(yy82, yy83000, yy831, yy82, yy83000)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 1 >= 4, 2 > 5
- new_span2Zs1(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs1(yy376, yy377, yy378, yy3790, yy3800)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_span2Ys0(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys1(yy66, yy67000, yy671, yy66, yy67000)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 1 >= 4, 2 > 5
- new_span2Ys1(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys1(yy370, yy371, yy372, yy3730, yy3740)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Zs0(yy376, yy378)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Zs1(yy376, yy377, yy378, Zero, Zero) → new_span2Ys0(yy376, yy378)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Zs0(yy370, yy372)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Ys1(yy370, yy371, yy372, Zero, Zero) → new_span2Ys0(yy370, yy372)
The graph contains the following edges 1 >= 1, 3 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_groupByZs0(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs0(yy189, yy190, yy191, yy1920, yy1930)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_groupByZs0(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs0(yy189, yy190, yy191, yy1920, yy1930)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_groupByYs0(yy142, yy143, yy144, Succ(yy1450), Succ(yy1460)) → new_groupByYs0(yy142, yy143, yy144, yy1450, yy1460)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_groupByYs0(yy142, yy143, yy144, Succ(yy1450), Succ(yy1460)) → new_groupByYs0(yy142, yy143, yy144, yy1450, yy1460)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Zs2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Zs2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Zs2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys2(:(Neg(Zero), yy3111)) → new_span2Ys2(yy3111)
The graph contains the following edges 1 > 1
- new_span2Ys2(:(Pos(Zero), yy3111)) → new_span2Ys2(yy3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Zs3(yy358, yy360)
new_span2Ys3(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys10(yy69, yy71000, yy711, yy69, yy71000)
new_span2Zs3(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs10(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Ys3(yy364, yy366)
new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Zs3(yy364, yy366)
new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Ys3(yy358, yy360)
new_span2Zs10(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs10(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys10(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys10(yy358, yy359, yy360, yy3610, yy3620)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs3(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs10(yy76, yy77000, yy771, yy76, yy77000)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 1 >= 4, 2 > 5
- new_span2Ys10(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys10(yy358, yy359, yy360, yy3610, yy3620)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_span2Ys3(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys10(yy69, yy71000, yy711, yy69, yy71000)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 1 >= 4, 2 > 5
- new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Ys3(yy358, yy360)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Ys10(yy358, yy359, yy360, Zero, Zero) → new_span2Zs3(yy358, yy360)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Ys3(yy364, yy366)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Zs10(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs10(yy364, yy365, yy366, yy3670, yy3680)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
- new_span2Zs10(yy364, yy365, yy366, Zero, Zero) → new_span2Zs3(yy364, yy366)
The graph contains the following edges 1 >= 1, 3 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_groupByZs00(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs00(yy183, yy184, yy185, yy1860, yy1870)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_groupByZs00(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs00(yy183, yy184, yy185, yy1860, yy1870)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_groupByYs00(yy136, yy137, yy138, Succ(yy1390), Succ(yy1400)) → new_groupByYs00(yy136, yy137, yy138, yy1390, yy1400)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_groupByYs00(yy136, yy137, yy138, Succ(yy1390), Succ(yy1400)) → new_groupByYs00(yy136, yy137, yy138, yy1390, yy1400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))
The TRS R consists of the following rules:
new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
The set Q consists of the following terms:
new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_groupBy(:(yy30, yy31)) → new_groupBy(new_groupByZs01(yy30, yy31))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2
POL(Neg(x1)) = 0
POL(Pos(x1)) = 0
POL(Succ(x1)) = 0
POL(Zero) = 0
POL([]) = 0
POL(new_groupBy(x1)) = x1
POL(new_groupByZs01(x1, x2)) = x2
POL(new_groupByZs02(x1, x2, x3)) = 1 + x3
POL(new_groupByZs03(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_groupByZs04(x1, x2, x3, x4, x5)) = x5
POL(new_groupByZs05(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_groupByZs06(x1, x2, x3)) = 1 + x3
POL(new_groupByZs07(x1, x2, x3, x4, x5)) = x5
POL(new_span2Ys11(x1, x2, x3)) = 1 + x2
POL(new_span2Ys110(x1, x2, x3)) = 1 + x2
POL(new_span2Ys12(x1, x2, x3)) = 1 + x2
POL(new_span2Ys13(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Ys14(x1, x2, x3)) = 0
POL(new_span2Ys15(x1, x2, x3, x4, x5)) = 1 + x4
POL(new_span2Ys16(x1, x2, x3, x4, x5)) = 1 + x4
POL(new_span2Ys17(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Ys18(x1, x2, x3)) = 0
POL(new_span2Ys19(x1, x2, x3)) = 1 + x2
POL(new_span2Ys4(x1, x2)) = x2
POL(new_span2Ys5(x1)) = x1
POL(new_span2Ys6(x1, x2)) = x2
POL(new_span2Ys7(x1)) = x1
POL(new_span2Zs11(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Zs110(x1, x2, x3)) = x3
POL(new_span2Zs12(x1, x2, x3)) = 1 + x3
POL(new_span2Zs13(x1, x2, x3, x4, x5)) = 1 + x5
POL(new_span2Zs14(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Zs15(x1, x2, x3)) = x3
POL(new_span2Zs16(x1, x2, x3)) = x3
POL(new_span2Zs17(x1, x2, x3)) = 1 + x3
POL(new_span2Zs18(x1, x2, x3)) = 1 + x3
POL(new_span2Zs19(x1, x2, x3, x4, x5)) = x5
POL(new_span2Zs4(x1, x2)) = x2
POL(new_span2Zs5(x1)) = x1
POL(new_span2Zs6(x1, x2)) = x2
POL(new_span2Zs7(x1)) = x1
The following usable rules [17] were oriented:
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Ys4(yy66, []) → []
new_groupByZs01(yy30, []) → []
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys14(yy370, yy371, yy372) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5([]) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys6(yy69, []) → []
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys5([]) → []
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Ys7([]) → []
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs7([]) → []
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Zs4(yy82, []) → []
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs110(yy3111, yy17, yy16) → yy16
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_span2Ys6(yy69, :(Pos(Succ(yy71000)), yy711)) → new_span2Ys17(yy69, yy71000, yy711, yy69, yy71000)
new_span2Ys6(yy69, []) → []
new_span2Ys110(yy3111, yy11, yy10) → :(Neg(Zero), yy11)
new_span2Zs13(yy376, yy377, yy378, yy388, yy387) → yy387
new_span2Ys11(yy3111, yy5, yy4) → :(Pos(Zero), yy5)
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Succ(yy3680)) → new_span2Zs14(yy364, yy365, yy366, yy3670, yy3680)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Succ(yy3620)) → new_span2Ys17(yy358, yy359, yy360, yy3610, yy3620)
new_span2Zs7(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Neg(Succ(yy67000)), yy671)) → new_span2Ys13(yy66, yy67000, yy671, yy66, yy67000)
new_span2Zs16(yy3111, yy13, yy12) → yy12
new_span2Ys7(:(Neg(Zero), yy3111)) → new_span2Ys110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Zs110(yy3111, yy17, yy16) → yy16
new_groupByZs03(yy189, yy190, yy191, Zero, Zero) → new_groupByZs04(yy189, yy190, yy191, new_span2Ys4(yy189, yy191), new_span2Zs4(yy189, yy191))
new_groupByZs01(yy30, []) → []
new_span2Ys6(yy69, :(Neg(yy7100), yy711)) → []
new_span2Ys17(yy358, yy359, yy360, Zero, Succ(yy3620)) → new_span2Ys18(yy358, yy359, yy360)
new_span2Ys17(yy358, yy359, yy360, Succ(yy3610), Zero) → new_span2Ys18(yy358, yy359, yy360)
new_span2Zs7(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Ys4(yy66, :(Pos(yy6700), yy671)) → []
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Succ(yy31000)), yy311)) → new_groupByZs03(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Ys15(yy370, yy371, yy372, yy386, yy385) → :(Neg(Succ(yy371)), yy386)
new_span2Ys7(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs4(yy82, :(Neg(Succ(yy83000)), yy831)) → new_span2Zs11(yy82, yy83000, yy831, yy82, yy83000)
new_span2Ys16(yy358, yy359, yy360, yy382, yy381) → :(Pos(Succ(yy359)), yy382)
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Succ(yy1930)) → new_groupByZs03(yy189, yy190, yy191, yy1920, yy1930)
new_groupByZs01(Pos(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_span2Ys13(yy370, yy371, yy372, Zero, Succ(yy3740)) → new_span2Ys14(yy370, yy371, yy372)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Zero) → new_span2Ys14(yy370, yy371, yy372)
new_span2Zs4(yy82, :(Neg(Zero), yy831)) → :(Neg(Zero), yy831)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Succ(yy1870)) → new_groupByZs05(yy183, yy184, yy185, yy1860, yy1870)
new_span2Ys5(:(Neg(Succ(yy311000)), yy3111)) → []
new_span2Zs5([]) → []
new_span2Zs14(yy364, yy365, yy366, Zero, Zero) → new_span2Zs19(yy364, yy365, yy366, new_span2Ys6(yy364, yy366), new_span2Zs6(yy364, yy366))
new_groupByZs01(Pos(Succ(yy3000)), :(Neg(yy3100), yy311)) → :(Neg(yy3100), yy311)
new_groupByZs01(Neg(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
new_groupByZs02(yy189, yy190, yy191) → :(Neg(Succ(yy190)), yy191)
new_groupByZs01(Neg(Succ(yy3000)), :(Neg(Zero), yy311)) → :(Neg(Zero), yy311)
new_span2Zs7(:(Neg(Zero), yy3111)) → new_span2Zs15(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys19(yy3111, yy9, yy8) → :(Pos(Zero), yy9)
new_groupByZs01(Neg(Zero), :(Neg(Zero), yy311)) → new_span2Zs7(yy311)
new_groupByZs05(yy183, yy184, yy185, Zero, Succ(yy1870)) → new_groupByZs06(yy183, yy184, yy185)
new_groupByZs05(yy183, yy184, yy185, Succ(yy1860), Zero) → new_groupByZs06(yy183, yy184, yy185)
new_span2Zs17(yy3111, yy15, yy14) → yy14
new_span2Zs14(yy364, yy365, yy366, Succ(yy3670), Zero) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs14(yy364, yy365, yy366, Zero, Succ(yy3680)) → new_span2Zs18(yy364, yy365, yy366)
new_span2Zs6(yy76, :(Pos(Succ(yy77000)), yy771)) → new_span2Zs14(yy76, yy77000, yy771, yy76, yy77000)
new_span2Zs5(:(Pos(Zero), yy3111)) → new_span2Zs16(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Ys18(yy358, yy359, yy360) → []
new_span2Ys5(:(Neg(Zero), yy3111)) → new_span2Ys12(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs5(:(Neg(Succ(yy311000)), yy3111)) → :(Neg(Succ(yy311000)), yy3111)
new_span2Zs19(yy364, yy365, yy366, yy384, yy383) → yy383
new_span2Zs7(:(Pos(Zero), yy3111)) → new_span2Zs110(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_groupByZs01(Neg(Zero), :(Pos(Zero), yy311)) → new_span2Zs7(yy311)
new_span2Ys17(yy358, yy359, yy360, Zero, Zero) → new_span2Ys16(yy358, yy359, yy360, new_span2Ys6(yy358, yy360), new_span2Zs6(yy358, yy360))
new_span2Zs11(yy376, yy377, yy378, Zero, Succ(yy3800)) → new_span2Zs12(yy376, yy377, yy378)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Zero) → new_span2Zs12(yy376, yy377, yy378)
new_span2Ys6(yy69, :(Pos(Zero), yy711)) → []
new_groupByZs06(yy183, yy184, yy185) → :(Pos(Succ(yy184)), yy185)
new_span2Zs11(yy376, yy377, yy378, Zero, Zero) → new_span2Zs13(yy376, yy377, yy378, new_span2Ys4(yy376, yy378), new_span2Zs4(yy376, yy378))
new_span2Zs4(yy82, :(Pos(yy8300), yy831)) → :(Pos(yy8300), yy831)
new_span2Zs6(yy76, :(Neg(yy7700), yy771)) → :(Neg(yy7700), yy771)
new_span2Zs5(:(Neg(Zero), yy3111)) → new_span2Zs17(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_groupByZs01(Pos(Zero), :(Neg(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Zs12(yy376, yy377, yy378) → :(Neg(Succ(yy377)), yy378)
new_span2Ys7(:(Pos(Zero), yy3111)) → new_span2Ys19(yy3111, new_span2Ys7(yy3111), new_span2Zs7(yy3111))
new_span2Ys5([]) → []
new_groupByZs05(yy183, yy184, yy185, Zero, Zero) → new_groupByZs07(yy183, yy184, yy185, new_span2Ys6(yy183, yy185), new_span2Zs6(yy183, yy185))
new_groupByZs03(yy189, yy190, yy191, Succ(yy1920), Zero) → new_groupByZs02(yy189, yy190, yy191)
new_groupByZs03(yy189, yy190, yy191, Zero, Succ(yy1930)) → new_groupByZs02(yy189, yy190, yy191)
new_span2Ys13(yy370, yy371, yy372, Succ(yy3730), Succ(yy3740)) → new_span2Ys13(yy370, yy371, yy372, yy3730, yy3740)
new_span2Zs7([]) → []
new_groupByZs04(yy189, yy190, yy191, yy201, yy200) → yy200
new_span2Ys12(yy3111, yy7, yy6) → :(Neg(Zero), yy7)
new_span2Zs11(yy376, yy377, yy378, Succ(yy3790), Succ(yy3800)) → new_span2Zs11(yy376, yy377, yy378, yy3790, yy3800)
new_span2Ys4(yy66, []) → []
new_span2Ys7([]) → []
new_span2Zs18(yy364, yy365, yy366) → :(Pos(Succ(yy365)), yy366)
new_groupByZs01(Neg(Succ(yy3000)), :(Pos(yy3100), yy311)) → :(Pos(yy3100), yy311)
new_span2Zs4(yy82, []) → []
new_span2Ys5(:(Pos(Zero), yy3111)) → new_span2Ys11(yy3111, new_span2Ys5(yy3111), new_span2Zs5(yy3111))
new_span2Zs6(yy76, []) → []
new_span2Ys13(yy370, yy371, yy372, Zero, Zero) → new_span2Ys15(yy370, yy371, yy372, new_span2Ys4(yy370, yy372), new_span2Zs4(yy370, yy372))
new_span2Ys7(:(Pos(Succ(yy311000)), yy3111)) → []
new_groupByZs07(yy183, yy184, yy185, yy199, yy198) → yy198
new_span2Zs6(yy76, :(Pos(Zero), yy771)) → :(Pos(Zero), yy771)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Succ(yy31000)), yy311)) → new_groupByZs05(yy3000, yy31000, yy311, yy3000, yy31000)
new_span2Zs5(:(Pos(Succ(yy311000)), yy3111)) → :(Pos(Succ(yy311000)), yy3111)
new_groupByZs01(Neg(Zero), :(Neg(Succ(yy31000)), yy311)) → :(Neg(Succ(yy31000)), yy311)
new_groupByZs01(Pos(Succ(yy3000)), :(Pos(Zero), yy311)) → :(Pos(Zero), yy311)
new_span2Ys5(:(Pos(Succ(yy311000)), yy3111)) → []
new_span2Ys14(yy370, yy371, yy372) → []
new_groupByZs01(Pos(Zero), :(Pos(Zero), yy311)) → new_span2Zs5(yy311)
new_span2Ys4(yy66, :(Neg(Zero), yy671)) → []
new_span2Zs15(yy3111, yy19, yy18) → yy18
new_groupByZs01(Pos(Zero), :(Pos(Succ(yy31000)), yy311)) → :(Pos(Succ(yy31000)), yy311)
The set Q consists of the following terms:
new_span2Zs15(x0, x1, x2)
new_span2Zs7([])
new_span2Zs14(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys17(x0, x1, x2, Zero, Succ(x3))
new_span2Ys6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys12(x0, x1, x2)
new_span2Zs4(x0, [])
new_span2Zs18(x0, x1, x2)
new_span2Zs11(x0, x1, x2, Zero, Succ(x3))
new_span2Zs110(x0, x1, x2)
new_span2Zs7(:(Pos(Succ(x0)), x1))
new_span2Ys14(x0, x1, x2)
new_span2Zs5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Succ(x3), Zero)
new_span2Ys5(:(Pos(Succ(x0)), x1))
new_span2Zs11(x0, x1, x2, Zero, Zero)
new_span2Zs19(x0, x1, x2, x3, x4)
new_span2Ys7([])
new_span2Ys11(x0, x1, x2)
new_groupByZs01(Pos(Zero), :(Pos(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Succ(x3))
new_span2Zs7(:(Neg(Zero), x0))
new_span2Zs14(x0, x1, x2, Succ(x3), Zero)
new_span2Ys110(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Zero), :(Pos(Zero), x0))
new_groupByZs07(x0, x1, x2, x3, x4)
new_span2Zs5(:(Neg(Succ(x0)), x1))
new_groupByZs02(x0, x1, x2)
new_span2Ys7(:(Pos(Succ(x0)), x1))
new_span2Ys4(x0, :(Pos(x1), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Neg(Zero), x0))
new_span2Zs13(x0, x1, x2, x3, x4)
new_span2Ys16(x0, x1, x2, x3, x4)
new_span2Zs4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys7(:(Neg(Succ(x0)), x1))
new_span2Ys7(:(Neg(Zero), x0))
new_span2Ys17(x0, x1, x2, Zero, Zero)
new_groupByZs01(Neg(Succ(x0)), :(Pos(x1), x2))
new_groupByZs01(Neg(Succ(x0)), :(Neg(Succ(x1)), x2))
new_groupByZs03(x0, x1, x2, Succ(x3), Succ(x4))
new_groupByZs05(x0, x1, x2, Zero, Succ(x3))
new_span2Ys5(:(Neg(Zero), x0))
new_span2Ys19(x0, x1, x2)
new_span2Zs5(:(Pos(Zero), x0))
new_groupByZs01(Pos(Succ(x0)), :(Pos(Zero), x1))
new_groupByZs05(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys4(x0, :(Neg(Zero), x1))
new_span2Ys5(:(Neg(Succ(x0)), x1))
new_groupByZs01(Neg(Zero), :(Neg(Succ(x0)), x1))
new_span2Ys6(x0, [])
new_groupByZs01(Neg(Succ(x0)), :(Neg(Zero), x1))
new_span2Ys6(x0, :(Neg(x1), x2))
new_span2Zs12(x0, x1, x2)
new_groupByZs01(Neg(Zero), :(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Zero)
new_span2Zs11(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs16(x0, x1, x2)
new_span2Ys5(:(Pos(Zero), x0))
new_span2Ys6(x0, :(Pos(Zero), x1))
new_span2Zs17(x0, x1, x2)
new_span2Ys4(x0, [])
new_groupByZs01(x0, [])
new_span2Zs4(x0, :(Pos(x1), x2))
new_span2Zs6(x0, :(Pos(Succ(x1)), x2))
new_span2Ys13(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Ys5([])
new_span2Zs6(x0, [])
new_span2Ys7(:(Pos(Zero), x0))
new_span2Ys17(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Neg(Zero), :(Pos(Succ(x0)), x1))
new_span2Ys17(x0, x1, x2, Succ(x3), Succ(x4))
new_span2Zs4(x0, :(Neg(Zero), x1))
new_groupByZs06(x0, x1, x2)
new_groupByZs05(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Succ(x0)), :(Neg(x1), x2))
new_span2Zs14(x0, x1, x2, Zero, Succ(x3))
new_groupByZs01(Pos(Zero), :(Neg(Succ(x0)), x1))
new_groupByZs03(x0, x1, x2, Zero, Zero)
new_span2Ys13(x0, x1, x2, Succ(x3), Zero)
new_groupByZs01(Pos(Zero), :(Pos(Zero), x0))
new_span2Zs5([])
new_span2Zs7(:(Pos(Zero), x0))
new_span2Ys15(x0, x1, x2, x3, x4)
new_groupByZs01(Pos(Succ(x0)), :(Pos(Succ(x1)), x2))
new_span2Zs14(x0, x1, x2, Zero, Zero)
new_groupByZs04(x0, x1, x2, x3, x4)
new_span2Zs6(x0, :(Pos(Zero), x1))
new_span2Zs6(x0, :(Neg(x1), x2))
new_span2Ys4(x0, :(Neg(Succ(x1)), x2))
new_span2Ys18(x0, x1, x2)
new_span2Zs7(:(Neg(Succ(x0)), x1))
new_span2Zs5(:(Neg(Zero), x0))
new_span2Ys13(x0, x1, x2, Zero, Succ(x3))
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.